<?php
# get new basename or use the one we have been using for this session
  $rname = rand();
  $tname = date('Y-m-d');
  $basename="phastregexOut_" . "$tname" . "_" . "$rname";
if($_SESSION['basename'] != NULL) {
  $basename = $_SESSION['basename']; #if we already have one, rather use that.
}
$_SESSION['basename'] = $basename;
$phastregex2path = "/home/x/Code/WEB_PHASTREGEX";
$workingdirectory = "/home/x/Public/phastregex2/work";
$working_address = "http://localhost/phastregex2/work";
?>   
